1. $i$ : $\mathbb{N}$
\\[0ex]2. $f$ : \{$f$ $\mid$ $i$:\{$z$:$\mathbb{N}\mid$ $z$ ($\lambda$$i$,$j$. $i$ $<$ $j$) $i$\}  $\rightarrow$ if ($i$ =$_{0}$ 0) then $\mathbb{Z}$ else \{$f$($i$ {-} 1)$\ldots\,$\} fi \}
\\[0ex]$\vdash$  if ($i$ =$_{0}$ 0) then $\mathbb{Z}$ else \{$f$($i$ {-} 1)$\ldots\,$\} fi  $\in$ Type